Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: set priority in monadic class instances #6725

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

JovanGerb
Copy link
Contributor

This PR changes the priority of some instances with monad transformers, most notably adding high priority to MonadExceptOf ε (ExceptT ε m). This means that in ExceptT α MetaM, throw will now throw the α instead of the Exception.

These instances now have high priority:

  • MonadReaderOf ρ (ReaderT ρ m)
  • MonadWithReaderOf ρ (ReaderT ρ m)
  • MonadStateOf σ (StateT σ m)
  • MonadStateOf σ (EStateT ε σ m)
  • MonadExceptOf ε (ExceptT ε m)
  • MonadExceptOf ε (EStateT ε σ m)
  • MonadExceptOf ε (ExceptCpsT ε m)
  • MonadCallStackOf κ (CallStackT κ m)
  • MonadCycleOf κ (CycleT κ m)

And these instance now have low priority:

  • MonadExceptOf Unit (OptionT m)
  • [MonadExcept ε m] {α : Type v} : OrElse (m α)

The last one makes sure that the OrElse instance has lower priority than instOrElseOfAlternative (this change doesn't affect the synthesis order, because the order of the files in which the instances were declared was already 'correct').

In Prelude.lean, instead of setting the priority to high or low, it has to be set to 10000 or 100, which is the same.

The increased priority of MonadExceptOf ε (ExceptT ε m) affected a few files that had to be fixed.

Closes #4212

@JovanGerb JovanGerb requested a review from tydeu as a code owner January 21, 2025 13:13
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 21, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 21, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 21, 2025
@JovanGerb
Copy link
Contributor Author

!bench

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 21, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@Kha
Copy link
Member

Kha commented Jan 28, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit f0232ae.
There were significant changes against commit f9e904a:

  Benchmark                   Metric          Change
  ============================================================
- big_omega.lean MT           branch-misses     6.9%  (16.8 σ)
- bv_decide_inequality.lean   branch-misses     1.2%  (13.6 σ)
- bv_decide_mul               branch-misses     2.6%  (13.6 σ)
- bv_decide_realworld         branch-misses     1.4%  (14.1 σ)
- lake build clean            wall-clock        1.2%  (18.6 σ)
+ language server startup     maxrss           -1.1% (-14.7 σ)

@JovanGerb
Copy link
Contributor Author

I think this is noise again.

@JovanGerb
Copy link
Contributor Author

It seems like for some tests the standard deviation isn't calibrated correctly.

@nomeata
Copy link
Collaborator

nomeata commented Jan 28, 2025

We briefly looked at this PR, and found that it’s not quite there yet:

  • all new priority assignemnts ideally come with a short comment referencing a Note that explains the design of these priorities, so that in the future a developer can understand the why of these priorities
  • I'd expect a test case to come with it that shows what was broken before and is now fixed.

As this fixes a P-low issue, ideally not too much effort will be spent on this, by you and the reviewers.

@nomeata nomeata added the awaiting-author Waiting for PR author to address issues label Jan 28, 2025
@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Jan 28, 2025
@github-actions github-actions bot added the stale label Feb 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author Waiting for PR author to address issues builds-mathlib CI has verified that Mathlib builds against this PR P-low We are not planning to work on this issue stale toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

RFC: type class synthesis order when outParam has multiple possible values
5 participants